package za.org.meraka.cair.ontorepair;

//Protege API Imports
import org.semanticweb.owlapi.apibinding.OWLManager;
import org.protege.editor.owl.model.OWLModelManager;
import org.semanticweb.owlapi.reasoner.OWLReasoner;
import org.semanticweb.owlapi.reasoner.OWLReasonerFactory;
import org.semanticweb.owlapi.reasoner.structural.StructuralReasonerFactory;
import org.semanticweb.owlapi.util.*;
import org.semanticweb.owlapi.model.*;
//import org.semanticweb.owlapi.inference.*; 

//Java API Imports
import java.util.Stack;
import java.util.Set;
import java.util.HashSet;
import java.net.URI;
import java.util.List;
import java.util.ArrayList;
import java.util.Collections; 

public class JustificationGenerator {
	private OWLModelManager modelManager;
	private OWLOntologyManager ontologyManager;
	private OWLReasoner reasoner;
	private OWLOntology logicalOntology;
	private OWLDataFactory dataF;
	private OWLReasonerFactory reasonerFactory;
																		
	private int depth, endC;				
	private Set<Set<OWLAxiom>> hittingSets,paths;
	private Set<OWLAxiom> justif;	
	private Set<Stack<Integer>> allPaths;
	private Stack<Integer> stack;
	private Stack<Set<OWLAxiom>> hsStack;
	private boolean end,superset;			
	private UtilityClass<OWLAxiom> utilCls;		 	
	private HSGenerator<OWLAxiom> g;
	private UtilityClass<OWLAxiom> ut;	
	private Signature sig;	
	public int rootJCount;
	private Set<Justification> justifications;
	private HashSet<OWLOntology> notEntailedCache;
	private HashSet<OWLOntology> entailedCache;
	
	public int perJRoot;
	public int perJNaive;
	
	public int totalRoot;
	public int totalNaive;
	public int jCount;
	public int duplicates;
	public long wastedTime;
	
	private Set<AxiomDescTuple> entailments;
	private Set<OWLClassExpression> unsatisConcepts;
	private AxiomNumberChecker numberChecker;
	
	public JustificationGenerator(){}
			
	public JustificationGenerator(OWLModelManager model, Signature s, OWLOntology m) throws OWLException{
		wastedTime = 0;
		notEntailedCache = new HashSet<OWLOntology>();
		entailedCache = new HashSet<OWLOntology>();
		
		numberChecker = new AxiomNumberChecker(m);
		dataF = model.getOWLDataFactory();
		//bruteForceSatisfiabilityCount = cleverSatisfiabilityCount = 0;
		perJRoot = perJNaive = totalRoot = totalNaive = jCount = duplicates = 0;
		sig = s;
		ut = new UtilityClass<OWLAxiom>();utilCls = new UtilityClass<OWLAxiom>();
		depth = 0;endC = 0;end = superset = false;
		stack = new Stack<Integer>();hittingSets = paths = new HashSet<Set<OWLAxiom>>();						
		hsStack = new Stack<Set<OWLAxiom>>();
		allPaths = new HashSet<Stack<Integer>>();
		
		justifications = new HashSet<Justification>();
		modelManager = model;									
   	    ontologyManager = OWLManager.createOWLOntologyManager();
   	    //reasoner = modelManager.getOWLReasonerManager().createReasoner(ontologyManager);
   	    //reasoner = modelManager.getReasoner();
   	    //reasonerFactory = new StructuralReasonerFactory(); 
		//reasoner = reasonerFactory.createReasoner(m);
   	    reasoner = modelManager.getOWLReasonerManager().getCurrentReasoner();
	}	
	
	public JustificationGenerator(OWLModelManager model, Set<AxiomDescTuple> e, Signature s, OWLOntology m) throws OWLException{
		//notEntailedCache = new HashSet<OWLOntology>();
		//entailedCache    = new HashSet<OWLOntology>();
		numberChecker = new AxiomNumberChecker(m);
		unsatisConcepts = new HashSet<OWLClassExpression>();
		for (AxiomDescTuple adT: e)
			unsatisConcepts.add(adT.desc);
						
		entailments = new HashSet<AxiomDescTuple>();entailments.addAll(e);
		dataF = model.getOWLDataFactory();		
		perJRoot = perJNaive = totalRoot = totalNaive = rootJCount = 0;
		//bruteForceSatisfiabilityCount = cleverSatisfiabilityCount = rootJCount = 0;
		sig = s;
		ut = new UtilityClass<OWLAxiom>();utilCls = new UtilityClass<OWLAxiom>();
		depth = 0;endC = 0;end = superset = false;
		stack = new Stack<Integer>();hittingSets = paths = new HashSet<Set<OWLAxiom>>();						
		hsStack = new Stack<Set<OWLAxiom>>();
		allPaths = new HashSet<Stack<Integer>>();
		
		justifications = new HashSet<Justification>();
		modelManager = model;									
   	    ontologyManager = OWLManager.createOWLOntologyManager();
   	    //reasoner = modelManager.getOWLReasonerManager().createReasoner(ontologyManager);  
   	    reasoner = modelManager.getOWLReasonerManager().getCurrentReasoner();
	}		
	
	private boolean lookupSuperset(OWLOntology ontology){
		HashSet<OWLOntology> tmpCache = new HashSet<OWLOntology>();
		Set<OWLAxiom> set = ontology.getAxioms();
		
		for (OWLOntology compSet: entailedCache){
			Set<OWLAxiom> tmp = compSet.getAxioms();
			if (set.containsAll(tmp)){
				tmpCache.add(compSet);				
			}
		}
		
		tmpCache.add(ontology);
		entailedCache = tmpCache;
		if (entailedCache.size() > 0)
			return true;
		
		return false;
	}
	
	private boolean lookupSubset(OWLOntology ontology){
		HashSet<OWLOntology> tmpCache = new HashSet<OWLOntology>();
		Set<OWLAxiom> set = ontology.getAxioms();
		
		for (OWLOntology compSet: notEntailedCache){
			Set<OWLAxiom> tmp = compSet.getAxioms();
			if (tmp.containsAll(set)){
				tmpCache.add(compSet);	
			}
		}
		
		tmpCache.add(ontology);
		notEntailedCache = tmpCache;
		if (notEntailedCache.size() > 0)
			return true;
		
		return false;
	}
	
	private boolean holds(OWLReasoner reasoner, OWLOntology ontology, OWLClassExpression desc) throws OWLException{
		if (notEntailedCache.isEmpty() || entailedCache.isEmpty()){
			perJNaive++;
			if (!reasoner.isSatisfiable(desc)){
				entailedCache.add(ontology);
				return true;
			}
			else{
				//notEntailedCache.add(ontology);
				return false;
			}
		}
		else{
			if (!entailedCache.isEmpty()){
				if (lookupSuperset(ontology)){//if ontology is a superset/equal to any entailedCache item then return true else false;
					return true;
				}
				return false;
			}				
			else if (!notEntailedCache.isEmpty()){
				if (lookupSubset(ontology)){//if ontology is subset/equal to any notEntailedCache item then return true else false;
					return false;
				}
				return false;
			}			
			else{
				perJNaive++;
				if (!reasoner.isSatisfiable(desc)){							
					entailedCache.add(ontology);
					return true;
				}
				else{
					notEntailedCache.add(ontology);
					return false;
				}
			}			
		}
	}
	
	public Set<OWLAxiom> simpleBlackBox(OWLClassExpression desc, OWLOntology ontology, OWLOntologyManager man) throws OWLException{
			System.out.println("got here");
			Set<OWLAxiom> axioms = ontology.getAxioms();
	    	for (OWLAxiom tmp: axioms){
	    		RemoveAxiom rem = new RemoveAxiom(ontology, tmp);
	    		man.applyChange(rem);
	    		reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(ontology);
	    		if (!holds(reasoner, ontology, desc)){
	    			AddAxiom add = new AddAxiom(ontology, tmp);
	    			man.applyChange(add);
	    		}
	    	}   	    	   	    	   	    
	    	return ontology.getAxioms();	
	}
	
	public Set<OWLAxiom> simpleBlackBoxUncached(OWLClassExpression desc, OWLOntology ontology, OWLOntologyManager man) throws OWLException{						
		Set<OWLAxiom> axioms = ontology.getAxioms();
    	for (OWLAxiom tmp: axioms){
    		RemoveAxiom rem = new RemoveAxiom(ontology, tmp);
    		man.applyChange(rem);
    		reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(ontology);
    		if (reasoner.isSatisfiable(desc)){
    			AddAxiom add = new AddAxiom(ontology, tmp);
    			man.applyChange(add);
    		}
    	}   	    	   	    	   	    
    	return ontology.getAxioms();	
}
		
	private int getWindowSize(int axiomCount){
		int result = 0;
		result = axiomCount/10;
		if (result > 10)
			return result;
		else
			return 10;
	}
		
	public boolean noneEntailed(OWLReasoner reasoner, Set<OWLClassExpression> descs) throws OWLException{
		for (OWLClassExpression desc: descs){
			perJRoot++;
			if (!reasoner.isSatisfiable(desc))
				return false;
		}
		return true;
	}
	
	public boolean someEntailed(OWLReasoner reasoner, Set<OWLClassExpression> descs) throws OWLException{
		for (OWLClassExpression desc: descs){
			perJRoot++;
			if (!reasoner.isSatisfiable(desc))
				return true;
		}
		return false;
	}
		
	/*private boolean someEntailed(OWLReasoner reasoner, OWLClassExpression desc) throws OWLException{
		//Set<OWLClassExpression> persisting = new HashSet<OWLClassExpression>();
		//for (OWLClassExpression d: ents){
		//}
		cleverSatisfiabilityCount++;
		if (!reasoner.isSatisfiable(desc))
			return true;

		return false;
	}*/
	
	
			
	public Set<OWLAxiom> getSingleRootJustification(Set<OWLClassExpression> descs, OWLOntology ontology) throws OWLException{				
		/**Extract a module: No need. Already done initial module extraction*/
		OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
		//reasoner = modelManager.getOWLReasonerManager().createReasoner(manager);
		//reasoner = modelManager.getReasoner();
		OWLOntology module = manager.createOntology(ontology.getAxioms());
		reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(module);
		//reasoner.loadOntologies(Collections.singleton(module));
		/*if (!someEntailed(reasoner, descs)){
			return new HashSet<OWLAxiom>();
		}*/
		if (noneEntailed(reasoner, descs)){
			return new HashSet<OWLAxiom>();
		}
		/**Perform expansion?*/		
		
		/**Perform contraction(Sliding Window)*/
		//2.2 Contraction
		List<OWLOntologyChange> adds = new ArrayList<OWLOntologyChange>();
		List<OWLOntologyChange> rems = new ArrayList<OWLOntologyChange>();   	  

		//2.2.1 Fast Contraction
		int len = 0;//module.getAxiomCount();		
		int windowS = getWindowSize(len);		
			    			   			
		OntologyPartitioner ap;
		Set<OWLAxiom> setAx;// = new HashSet<OWLAxiom>();	   			
		OWLAxiom [] setAx2;
				
		//Sliding Window
		while (windowS > 0){	    
			len = module.getAxiomCount();
			int t = len/windowS;
			if (t < 1) t = 1;
			ap = new OntologyPartitioner(module, t);
			
			for (int i = 0; i < t; i++){
				setAx = ap.getPart(i);
				setAx2 = (OWLAxiom[])setAx.toArray(new OWLAxiom[setAx.size()]);
				/*for (OWLAxiom axiom: setAx){
					rems.add(new RemoveAxiom(module, axiom));
					adds.add(new AddAxiom(module, axiom));
				}*/
				for (int j = 0; j < setAx2.length; j++){	    			
					rems.add(new RemoveAxiom(module, setAx2[j]));
					adds.add(new AddAxiom(module, setAx2[j]));
				}
				
				manager.applyChanges(rems);	   
				//reasoner.clearOntologies();
				//reasoner.loadOntologies(Collections.singleton(module));
				reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(module);
				
				if (!someEntailed(reasoner, descs)){
					manager.applyChanges(adds);					
				}
				/*if (noneEntailed(reasoner, descs)){
					manager.applyChanges(adds);
				}*/
				rems = new ArrayList<OWLOntologyChange>();
				adds = new ArrayList<OWLOntologyChange>();						
			}	    			
			windowS/=2;	    	
		}									
		
		return module.getAxioms();				
	}
		
	/**Return all entailments from the list that follow from the given sentences(rootJ).*/

	
	/**Compute Single Justification*/
 	public Set<OWLAxiom> getJustification(OWLClassExpression desc, OWLOntology ontology) throws OWLException{
		Set<OWLAxiom> justif = new HashSet<OWLAxiom>();
		
		//Create Temp Ontology: Tests entailment before expansion phase.
		OWLOntology tempOntology2;
		OWLOntologyManager manager2 = OWLManager.createOWLOntologyManager();
			
		IRI ontologyIRI3 = IRI.create("http://www.meraka.org.za/ontologies/main3.owl");
		IRI physicalIRI3 = IRI.create("file:/tmp/main3.owl");
		SimpleIRIMapper mapper3 = new SimpleIRIMapper(ontologyIRI3, physicalIRI3);
		manager2.addIRIMapper(mapper3);
	    
		tempOntology2 = manager2.createOntology(ontologyIRI3);
      	     	
		manager2.addAxioms(tempOntology2,ontology.getAxioms());					
					       	     											 						
			int parts = 0;
	   	    int axiomCount = tempOntology2.getAxiomCount();
	   	    if (axiomCount >= 10){
	   	    	parts = axiomCount/10;	   	    	
	   	    	if (parts >= 10)	   	    	
	   	    		parts = 10;
	   	    		   	       	    
	   	    	/*ModuleExtractor m2 = new ModuleExtractor();
	   	    	int count = 0;
	   	    	reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(tempOntology2);
	   	    	
	   	    	while (!holds(reasoner, tempOntology2, desc)){
	   			//while (reasoner.isSatisfiable(desc)){
	   				//notEntailedCache.add(tempOntology2);	   				
	   				count++;
	   				Set<OWLAxiom> currSet = m2.selectionFunction(ontology, sig, count);
	   				manager2.addAxioms(tempOntology2,currSet);
	   				//reasoner.clearOntologies();
	   	   			//reasoner.loadOntologies(Collections.singleton(tempOntology2));
	   				reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(tempOntology2);
	   			}*/				   			   	       	       	   		   			   	    	  
	   			
	   			//2.2 Contraction
	   			List<OWLOntologyChange> adds = new ArrayList<OWLOntologyChange>();
	   			List<OWLOntologyChange> rems = new ArrayList<OWLOntologyChange>();   	  
    
	   			//2.2.1 Fast Contraction
	   			int windowS = 0;	   				   			
	   			windowS = tempOntology2.getAxiomCount()/10;
	    		if (windowS < 10){   	    		   	    
	    			windowS = 10;   	    	
	    		}
	    
	   			int len = 0;	    
	   			len = tempOntology2.getAxiomCount();	   			
	   			OntologyPartitioner ap;
	   			Set<OWLAxiom> setAx;OWLAxiom [] setAx2;
	   			int size = len/windowS;	   			
	   			
	   			if (size == 0){	   			
	   				return simpleBlackBox(desc, tempOntology2, manager2);	   			   		
	   			}
	   		
	   			/**Ontology size > 10**/
	   			while (windowS > 0){	    	   				
	   				len = tempOntology2.getAxiomCount();	   				
	   				ap = new OntologyPartitioner(tempOntology2, len/windowS);	   				
	   				for (int i = 0; i < len/windowS; i++){
	   					setAx = ap.getPart(i);
	   					setAx2 = (OWLAxiom[])setAx.toArray(new OWLAxiom[setAx.size()]);
	   					for (int j = 0; j < setAx2.length; j++){	    			
	   						rems.add(new RemoveAxiom(tempOntology2, setAx2[j]));
	   						adds.add(new AddAxiom(tempOntology2, setAx2[j]));
	   					}	    		
	   					manager2.applyChanges(rems);	   
	   					//reasoner.clearOntologies();
	   					//reasoner.loadOntologies(Collections.singleton(tempOntology2));	 
	   					reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(tempOntology2);
	   					//if (reasoner.isSatisfiable(desc)){	   					
	   					if (!holds(reasoner, tempOntology2, desc)){	   		
	   						//notEntailedCache.add(tempOntology2);
	   						manager2.applyChanges(adds);	    		
	   					}	    			    		
	   					rems = new ArrayList<OWLOntologyChange>();
	   					adds = new ArrayList<OWLOntologyChange>();
	   				}	    	
	   				windowS/=2;	    	
	   			}		   	
	   			//System.out.println("ss");
	   			return tempOntology2.getAxioms();
	   	    }
	   	    else{
	   	    	/**Ontology size <= 10**/
	   	    	//System.out.println(tempOntology2.getAxiomCount());
	   	    	return simpleBlackBox(desc,tempOntology2, manager2);   	    	
	   		}				  	
	}
 	
 	/**Compute Single Justification*/
 	public Set<OWLAxiom> getJustificationUncached(OWLClassExpression desc, OWLOntology ontology) throws OWLException{
		Set<OWLAxiom> justif = new HashSet<OWLAxiom>();
		
		//Create Temp Ontology: Tests entailment before expansion phase.
		OWLOntology tempOntology2;
		OWLOntologyManager manager2 = OWLManager.createOWLOntologyManager();
			
		IRI ontologyIRI3 = IRI.create("http://www.meraka.org.za/ontologies/main3.owl");
		IRI physicalIRI3 = IRI.create("file:/tmp/main3.owl");
		SimpleIRIMapper mapper3 = new SimpleIRIMapper(ontologyIRI3, physicalIRI3);
		manager2.addIRIMapper(mapper3);
	    
		tempOntology2 = manager2.createOntology(ontologyIRI3);
      	     	
		manager2.addAxioms(tempOntology2,ontology.getAxioms());					
					       	     											 						
			int parts = 0;
	   	    int axiomCount = tempOntology2.getAxiomCount();
	   	    if (axiomCount >= 10){
	   	    	parts = axiomCount/10;	   	    	
	   	    	if (parts >= 10)	   	    	
	   	    		parts = 10;
	   	    		   	       	    
	   	    	ModuleExtractor m2 = new ModuleExtractor();
	   	    	int count = 0;
	   	    	//reasoner.clearOntologies();
	   	    	//reasoner.loadOntologies(Collections.singleton(tempOntology2));
	   	    		   	    	
	   			while (reasoner.isSatisfiable(desc)){
	   				//notEntailedCache.add(tempOntology2);	   				
	   				count++;
	   				Set<OWLAxiom> currSet = m2.selectionFunction(ontology, sig, count);
	   				manager2.addAxioms(tempOntology2,currSet);
	   				//reasoner.clearOntologies();
	   	   			//reasoner.loadOntologies(Collections.singleton(tempOntology2));	   					   				
	   			}				   			   	       	       	   		   			   	    	  
	   			
	   			//2.2 Contraction
	   			List<OWLOntologyChange> adds = new ArrayList<OWLOntologyChange>();
	   			List<OWLOntologyChange> rems = new ArrayList<OWLOntologyChange>();   	  
    
	   			//2.2.1 Fast Contraction
	   			int windowS = 0;	   				   			
	   			windowS = tempOntology2.getAxiomCount()/10;
	    		if (windowS < 10){   	    		   	    
	    			windowS = 10;   	    	
	    		}
	    
	   			int len = 0;	    
	   			len = tempOntology2.getAxiomCount();	   			
	   			OntologyPartitioner ap;
	   			Set<OWLAxiom> setAx;OWLAxiom [] setAx2;
	   			int size = len/windowS;	   			
	   			
	   			if (size == 0){	   			
	   				return simpleBlackBox(desc, tempOntology2, manager2);	   			   		
	   			}
	   		
	   			/**Ontology size > 10**/
	   			while (windowS > 0){	    	   				
	   				len = tempOntology2.getAxiomCount();	   				
	   				ap = new OntologyPartitioner(tempOntology2, len/windowS);	   				
	   				for (int i = 0; i < len/windowS; i++){
	   					setAx = ap.getPart(i);
	   					setAx2 = (OWLAxiom[])setAx.toArray(new OWLAxiom[setAx.size()]);
	   					for (int j = 0; j < setAx2.length; j++){	    			
	   						rems.add(new RemoveAxiom(tempOntology2, setAx2[j]));
	   						adds.add(new AddAxiom(tempOntology2, setAx2[j]));
	   					}	    		
	   					manager2.applyChanges(rems);	   
	   					//reasoner.clearOntologies();
	   					//reasoner.loadOntologies(Collections.singleton(tempOntology2));	   					
	   					if (reasoner.isSatisfiable(desc)){	   						   						   	
	   						//notEntailedCache.add(tempOntology2);
	   						manager2.applyChanges(adds);	    		
	   					}	    			    		
	   					rems = new ArrayList<OWLOntologyChange>();
	   					adds = new ArrayList<OWLOntologyChange>();
	   				}	    	
	   				windowS/=2;	    	
	   			}		   	
	   			//System.out.println("ss");
	   			return tempOntology2.getAxioms();
	   	    }
	   	    else{
	   	    	/**Ontology size <= 10**/
	   	    	//System.out.println(tempOntology2.getAxiomCount());
	   	    	return simpleBlackBox(desc,tempOntology2, manager2);   	    	
	   		}				  	
	}
	
	/**Computing all Justifications: Keep track of HS Paths*/	
	public Set<Set<OWLAxiom>> getAllJ(OWLClassExpression desc, OWLOntology ontology) throws OWLException{							
		//reasoner.clearOntologies();
		//reasoner.loadOntologies(Collections.singleton(ontology));
		if (!reasoner.isSatisfiable(desc)){
			System.out.println();System.out.println("Justification:");
			System.out.println("------------------------------------------------------------");			
			justif = getJustification(desc, ontology);			
			for (OWLAxiom a: justif){System.out.println(a + "\t" + utilCls.getIndex(a, logicalOntology));}
			System.out.println("------------------------------------------------------------");				
			hittingSets.add(justif);								
			OWLAxiom[] justi = (OWLAxiom[])justif.toArray(new OWLAxiom[justif.size()]);
			
			for (int i = 0; i < justi.length;i++){					
				if (i+1 == justi.length){
					if (depth == 0 || superset)
						end = true;					
					endC++;
				}						
				stack.push(utilCls.getIndex(justi[i], logicalOntology));depth++;
				System.out.println();System.out.println("Axiom Removed: " + justi[i] + "\t" + utilCls.getIndex(justi[i], logicalOntology));System.out.println();
				if (!utilCls.superSet(stack, allPaths)){											
					getAllJ(desc, utilCls.removeAxiom(justi[i], ontology));
				}
				else{
					stack.pop();
					superset = true;
				}
			}			
			return hittingSets;
		}
		else{					
			//System.out.println();System.out.println("Depth: " + depth);
			Stack<Integer> tmp = new Stack<Integer>();
			tmp.addAll(stack);
			allPaths.add(tmp);
			System.out.println("Paths:");
			utilCls.printStack(allPaths);
			
			if (!end){
				superset = false;
				for (int e = 0; e <= endC; e++){
					depth--;
					stack.pop();
				}
				endC = 0;
			}																							
			return hittingSets;
		}	
	}
	
	/**Computing All Justifications: branching on previous justifications*/ 	
	public Set<Set<OWLAxiom>> getJ(OWLClassExpression desc, OWLOntology ontology) throws OWLException{			
		//reasoner.clearOntologies();
		//reasoner.loadOntologies(Collections.singleton(ontology));
		if (holds(reasoner, ontology, desc)){
			System.out.println("Holds");
			//if (!reasoner.isSatisfiable(desc)){
			perJNaive = 0;
			System.gc();
			long start = System.currentTimeMillis(); 
			justif = getJustification(desc, ontology);
			long end = System.currentTimeMillis();
			/*System.out.println("Current Justification: ");			
			for (OWLAxiom axiom: justif){
				System.out.print(numberChecker.lookupAxiomNumber(axiom) + " ");				
			}			
			System.out.println();
			System.out.println("Entailment Checks: " + perJNaive + " tests");
			System.out.println("Ontology Size: " + ontology.getAxiomCount() + " axioms");
			System.out.println();*/
			
			jCount++;			
			totalNaive += perJNaive;
												
//			if (hittingSets.isEmpty()){
//				//hsStack.push(justif);
//				hittingSets.add(justif);
//				g = new HSGenerator<OWLAxiom>(hittingSets);				
//				paths = g.getHittingSets();
//				System.out.print("branches: ");
//				for (Set<OWLAxiom> tmp2: paths){
//					System.out.print("{ ");
//					for (OWLAxiom a: tmp2){
//						System.out.print(numberChecker.lookupAxiomNumber(a) + " ");
//					}
//					System.out.print(" }, ");				
//				}				
//				System.out.println();
//				
//				//System.out.print("Removing: ");
//				for (Set<OWLAxiom> tmp: paths){
//					/*System.out.print("{ ");
//					for (OWLAxiom a: tmp){
//						System.out.print(numberChecker.lookupAxiomNumber(a) + " ");
//					}
//					System.out.print(" }, ");
//					System.out.println();*/
//					getJ(desc, ut.removeAxioms(tmp, ontology));
//				}
//			}
			//else{				
				if (hittingSets.contains(justif)){
					wastedTime += (end - start);
					duplicates++;
				}
				
				hittingSets.add(justif);	
				g = new HSGenerator<OWLAxiom>(hittingSets);
				//g.setF(ut.getRelevantSets(hittingSets, hsStack));							
				paths = g.getHittingSets();
				//hsStack.push(justif);
				//System.out.print("branches: ");
				for (Set<OWLAxiom> tmp2: paths){
					//System.out.print("{ ");
					for (OWLAxiom a: tmp2){
						//System.out.print(numberChecker.lookupAxiomNumber(a) + " ");
					}
					//System.out.print(" }, ");				
				}				
				//System.out.println();
				
				//System.out.print("Removing: ");
				for (Set<OWLAxiom> tmp: paths){
					/*System.out.print("{ ");
					for (OWLAxiom a: tmp){
						System.out.print(numberChecker.lookupAxiomNumber(a) + " ");
					}
					System.out.print(" }");
					System.out.println();*/
					getJ(desc, ut.removeAxioms(tmp, ontology));
				}
			//}				
				
		if (!hsStack.isEmpty())
			hsStack.pop();
		}
		return hittingSets;		
	}
	
	/**Computing All Justifications: branching on previous justifications*/ 	
	public Set<Set<OWLAxiom>> getJUncached(OWLClassExpression desc, OWLOntology ontology) throws OWLException{			
		//reasoner.clearOntologies();
		//reasoner.loadOntologies(Collections.singleton(ontology));		
		if (!reasoner.isSatisfiable(desc)){
			perJNaive = 0;
			System.gc();
			long start = System.currentTimeMillis(); 
			justif = getJustification(desc, ontology);
			long end = System.currentTimeMillis();
			/*System.out.println("Current Justification: ");			
			for (OWLAxiom axiom: justif){
				System.out.print(numberChecker.lookupAxiomNumber(axiom) + " ");				
			}			
			System.out.println();
			System.out.println("Entailment Checks: " + perJNaive + " tests");
			System.out.println("Ontology Size: " + ontology.getAxiomCount() + " axioms");
			System.out.println();*/
			
			jCount++;			
			totalNaive += perJNaive;
												
//			if (hittingSets.isEmpty()){
//				//hsStack.push(justif);
//				hittingSets.add(justif);
//				g = new HSGenerator<OWLAxiom>(hittingSets);				
//				paths = g.getHittingSets();
//				System.out.print("branches: ");
//				for (Set<OWLAxiom> tmp2: paths){
//					System.out.print("{ ");
//					for (OWLAxiom a: tmp2){
//						System.out.print(numberChecker.lookupAxiomNumber(a) + " ");
//					}
//					System.out.print(" }, ");				
//				}				
//				System.out.println();
//				
//				//System.out.print("Removing: ");
//				for (Set<OWLAxiom> tmp: paths){
//					/*System.out.print("{ ");
//					for (OWLAxiom a: tmp){
//						System.out.print(numberChecker.lookupAxiomNumber(a) + " ");
//					}
//					System.out.print(" }, ");
//					System.out.println();*/
//					getJ(desc, ut.removeAxioms(tmp, ontology));
//				}
//			}
			//else{				
				if (hittingSets.contains(justif)){
					wastedTime += (end - start);
					duplicates++;
				}
				
				hittingSets.add(justif);	
				g = new HSGenerator<OWLAxiom>(hittingSets);
				//g.setF(ut.getRelevantSets(hittingSets, hsStack));							
				paths = g.getHittingSets();
				//hsStack.push(justif);
				System.out.print("branches: ");
				for (Set<OWLAxiom> tmp2: paths){
					System.out.print("{ ");
					for (OWLAxiom a: tmp2){
						System.out.print(numberChecker.lookupAxiomNumber(a) + " ");
					}
					System.out.print(" }, ");				
				}				
				System.out.println();
				
				//System.out.print("Removing: ");
				for (Set<OWLAxiom> tmp: paths){
					/*System.out.print("{ ");
					for (OWLAxiom a: tmp){
						System.out.print(numberChecker.lookupAxiomNumber(a) + " ");
					}
					System.out.print(" }");
					System.out.println();*/
					getJ(desc, ut.removeAxioms(tmp, ontology));
				}
			//}				
				
		if (!hsStack.isEmpty())
			hsStack.pop();
		}
		return hittingSets;		
	}

	/*private boolean checkHittingSets(Set<OWLClassExpression> ents, Set<Set<OWLAxiom>> hs, OWLReasoner reasoner, OWLOntology ontology)throws OWLException{
		boolean done = true;
		OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
		reasoner = modelManager.getOWLReasonerManager().createReasoner(manager);		
		OWLOntology tempOnt = manager.createOntology(ontology.getAxioms());		 
		reasoner.loadOntologies(Collections.singleton(tempOnt));
		
		//Set<OWLClassExpression> set = getPersistingEntailments(reasoner, ents);
		
		List<OWLOntologyChange> adds = new ArrayList<OWLOntologyChange>();
		List<OWLOntologyChange> rems = new ArrayList<OWLOntologyChange>();
		for (Set<OWLAxiom> just: hs){
			for (OWLAxiom ax: just){
				rems.add(new RemoveAxiom(tempOnt, ax));
				adds.add(new RemoveAxiom(tempOnt, ax));
			}				
		}
		
		manager.applyChanges(rems);
		reasoner.clearOntologies();
		reasoner.loadOntologies(Collections.singleton(tempOnt));
		//Set<OWLClassExpression> set2 = getPersistingEntailments(reasoner, ents);
		if (set2.size() > 0)
			done = false;		
		
		return done;
	}*/
	
	/**Computing All ROOT Justifications: branching on previous justifications*/ 	
	public void getRJ(OWLOntology ontology) throws OWLException{				
		//reasoner.clearOntologies();
		//reasoner.loadOntologies(Collections.singleton(ontology));	
		reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(ontology);
		while (someEntailed(reasoner, unsatisConcepts)){ 
			perJRoot = 0;
			justif = getSingleRootJustification(unsatisConcepts, ontology);
			rootJCount++;
			totalRoot += perJRoot;
			System.out.println("Current Root Justification: " + perJRoot + " tests");
			
			if (hittingSets.isEmpty()){
				hsStack.push(justif);
				int before = hittingSets.size();
				hittingSets.add(justif);
				int after = hittingSets.size();
				if (after > before && justif.size() > 0){									
					justifications.add(new Justification(modelManager, null, justif));
				}
				g = new HSGenerator<OWLAxiom>(hittingSets);
				paths = g.getHittingSets();
				for (Set<OWLAxiom> tmp: paths){				
					getRJ(ut.removeAxioms(tmp, ontology));
				}
			}
			else{				
				int before = hittingSets.size(); 
				hittingSets.add(justif);
				int after = hittingSets.size();
				if (after > before && justif.size() > 0){			
					justifications.add(new Justification(modelManager, null, justif));
				}
				g.setF(ut.getRelevantSets(hittingSets, hsStack));							
				paths = g.getHittingSets();
				hsStack.push(justif);
								
				for (Set<OWLAxiom> tmp: paths){				
					getRJ(ut.removeAxioms(tmp, ontology));
				}
			}					
		
		if (!hsStack.isEmpty())
			hsStack.pop();
		}
	}
	
	/**ROOT JUSTIFICATION VERSION: Computing root justifications*/
		
	/**Computing All Justifications: Core Algorithm*/	
	public Set<Set<OWLAxiom>> getMUPS(OWLClassExpression desc, OWLOntology ontology) throws OWLException{		
		//reasoner.clearOntologies();
		//reasoner.loadOntologies(Collections.singleton(ontology));		
		reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(ontology);
		if (!reasoner.isSatisfiable(desc)){								
				justif = getJustification(desc, ontology);				
				hittingSets.add(justif);							
				OWLAxiom[] justi = (OWLAxiom[])justif.toArray(new OWLAxiom[justif.size()]);									 
				for (int i = 0; i < justi.length;i++)
					getMUPS(desc, utilCls.removeAxiom(justi[i], ontology));
		}						
		return hittingSets;						
	}				
					
	/**Identify Necessary Axioms in justifications: Intersection of all justifications*/	
	public Set<OWLAxiom> getNecessaryAxioms(Set<OWLAxiom> justif, OWLClassExpression desc) throws OWLException{
		Set<OWLAxiom> necessaryAx = new HashSet<OWLAxiom>();		
		
		OWLOntology tempOntology;
		OWLOntologyManager ontologyManager = OWLManager.createOWLOntologyManager();
			
		IRI ontologyIRI3 = IRI.create("http://www.meraka.org.za/ontologies/main4.owl");
		IRI physicalIRI3 = IRI.create("file:/tmp/main4.owl");
		SimpleIRIMapper mapper3 = new SimpleIRIMapper(ontologyIRI3, physicalIRI3);
		ontologyManager.addIRIMapper(mapper3);
	    
		tempOntology = ontologyManager.createOntology(ontologyIRI3);
						
		//reasoner.clearOntologies();
		reasoner.dispose();	
		reasoner = modelManager.getReasoner();
   	    //reasoner = modelManager.getOWLReasonerManager().createReasoner(ontologyManager);
   	    ontologyManager.addAxioms(tempOntology,justif);
   	    //reasoner.loadOntologies(Collections.singleton(tempOntology));   	    
   	    											   	   
	   	for (OWLAxiom ax: tempOntology.getAxioms()){
	   	    	ontologyManager.applyChange(new RemoveAxiom(tempOntology, ax));
	   	    	//reasoner.clearOntologies();
	   	   	    //reasoner.loadOntologies(Collections.singleton(tempOntology));
	   	    	reasoner = modelManager.getOWLReasonerManager().getCurrentReasonerFactory().getReasonerFactory().createReasoner(tempOntology);
	   	    	
	   	    	if (reasoner.isSatisfiable(desc)){
	   	    		necessaryAx.add(ax);
	   	    		
	   	    	}	   	    	
	   	    	ontologyManager.applyChange(new AddAxiom(tempOntology, ax));
	   	}								
		return necessaryAx;
	}
	
	private boolean subSetOf(Justification j, Set<Justification> setJ){
		for (Justification j1: setJ){
			if (j1.justification.containsAll(j.justification) && (!j1.justification.equals(j.justification))){
				return true;
			}
		}
		return false;
	}
	
	public Set<Justification> getRoots(Set<Justification> justs){
		Set<Justification> r = new HashSet<Justification>();
		Set<Justification> tmp = new HashSet<Justification>();
		for (Justification j: justs){
			for (Justification j2: justs){
				if (!(j2.justification.equals(j.justification))){
					tmp.add(j2);
				}
			}
			if (!subSetOf(j, tmp)){
				r.add(j);
			}
			tmp = new HashSet<Justification>();
		}
		return r;
	}
	
	public Set<Justification> getRootJustifications(){
		/*AxiomPrinter p = new AxiomPrinter(modelManager);
		for (Set<OWLAxiom> s: hittingSets){
			System.out.println(p.printAxioms(s));
		}*/
		
		return justifications;
	}
}
